home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Language/OS - Multiplatform Resource Library
/
LANGUAGE OS.iso
/
quintus
/
quintus0.lha
/
work
/
hyper_2.06.2
< prev
next >
Wrap
Text File
|
1992-04-03
|
67KB
|
1,957 lines
%%% HYPER MATCHING
%%% version 2.00.7 (based on hyper_19.3)
%%% moved term rewriting to hypermatching
%%% version 2.00.9
%%% added bound on term rewriting
%%% version 2.01.0
%%% checked clause priority after each hyper-link
%%% version 2.01.3
%%% moved generation of rewrite rules to hyper-linking
%%% fixed bug when rewriting hyper-links from a unit nucleus
%%% added code to orient equations
%%% version 2.01.4
%%% modified rewriting of equations according to David Plaisted's method
%%% version 2.01.6
%%% sorted electrons by term size
%%% version 2.01.8
%%% recomputed variable list when rewriting hyper-link
%%% version 2.02.1
%%% added partial hyper-links to priority structure
%%% asserted over_priohm if priority exceeded during rewriting or
%%% hyper-linking
%%% fixed bug which counted hyper-links rejected after rewriting as good
%%% added partial rewrite count
%%% version 2.02.3
%%% deleted pulled out form of clauses whose priority is too large
%%% version 2.02.4
%%% fixed bugs when updating priority structure with partial hyper-link
%%% version 2.02.5
%%% fixed bug when updating priority structure with partial hyper-link
%%% version 2.02.7
%%% modified code so clauses corresponding to rewrite rules are not deleted
%%% version 2.02.8
%%% deleted rewrite rules when the priority of the lhs exceeds the priority
%%% bound
%%% version 2.02.9
%%% performed time overflow check after rejecting hyper-link due to priority
%%% version 2.03.0
%%% moved rewrite rule simplification to hyper-linking
%%% performed time overflow check after rejecting hyper-link due to relevance
%%% counted hyper-links rejected due to relevance as rejected
%%% version 2.03.1
%%% added early unit subsumption by X=X test
%%% version 2.03.2
%%% modified rewriting of equations so that equations are fully rewritten
%%% version 2.03.3
%%% strengthened early unit subsumption test so that partial hyper-links
%%% having all linked negative equations linked with X=X are tested
%%% using restricted rewrite
%%% fixed bug in the determination of linked and unlinked literals in partial
%%% hyper-links
%%% removed unit nucleus optimization from proc_C as modification for
%%% rewriting is more costly than normal processing
%%% removed unit nucleus optimization from calculate_new_size,
%%% calculate_priority_HM, make_varstail as it doesn't work with rewriting
%%% removed ground hyper-link optimization from calculate_new_size and
%%% calculate_priority_HM as it doesn't work with rewriting
%%% version 2.03.4
%%% incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
%%% are visible externally -- changes to comments, predicate names, and
%%% variable names are not incorporated
%%% printed deleting rewrite rule message only when outrwr set
%%% modified deleting rewrite rule message
%%% performed early unit subsumption test only when "equality_transform"
%%% version 2.03.5
%%% removed counters
%%% restored unit nucleus and ground nucleus optimizations to
%%% calculate_new_size, calculate_priority_HM, make_varstail, and
%%% proc_C when no rewrite rules
%%% version 2.03.6
%%% don't recalculate variable list after rewriting hyper-link as variable
%%% list is for nucleus
%%% version 2.03.9
%%% don't update priority structure in early priority test
%%% version 2.04.0
%%% performed unit deletion in early priority test
%%% logically erased nuclei while hyper-linking
%%% don't try to delete pulled out forms unless equality_transform set
%%% version 2.04.3
%%% erased corresponding equation and pulled out form when simplifying
%%% rewrite rule
%%% fixed rmrwr_prio so it erased all rewrite rules whose lhs was larger
%%% than the priority bound
%%% updated priority structure when early priority test succeeds
%%% version 2.04.4
%%% no longer pull out equations at the beginning of rounds
%%% version 2.04.5
%%% added equality_transform_by_round flag
%%% added safe_early_priority_test flag
%%% added early_unit_subsumption flag
%%% added early tautology test
%%% removed rewriting from hyper-linking
%%% removed the generation of rewrite rules from hyper-linking
%%% version 2.04.6
%%% added fixed_priority
%%% removed unnecessary checks for rewrite rules now that rewriting is no
%%% longer done in hyper-linking
%%% version 2.04.7
%%% added limited rewrite to hyper-linking
%%% moved code to erase clause corresponding to rewrite rule from
%%% erase_rewrite_rule to rmrwr_prio
%%% version 2.04.8
%%% fixed bug in early priority test which updated priority for partial
%%% instances which passed test instead of those which failed
%%% rewrote partial instance before early tautology test and early priority
%%% test
%%% version 2.05.0
%%% improved the efficiency of the unit deletion in early priority test
%%% checked for duplicate partial instances
%%% rejected a partial instance which is an instance of a previous partial
%%% instance only when delete_all_instances is set
%%% ordered early tests as early priority test, early tautology test,
%%% duplicate partial instance test, and early unit subsumption
%%% deleted a rewrite rule if its rhs priority is larger than the priority
%%% bound
%%% deleted a partial instance if its priority is larger than the priority
%%% bound
%%% rewrote literal before linking it
%%% erased partial instances for each nucleus
%%% version 2.05.3
%%% added support for Quintus Prolog
%%% fixed bug when updating priority structure after early priority failure
%%% modified rmhm_prio to delete equations corresponding to rewrite rules
%%% if their priority exceeds priority bound
%%% modified rmhm_prio not to delete pulled out forms when deleting a clause
%%% modified update_priority_structure to delete partial instances whose
%%% priority exceeds the priority bound
%%% updated priority structure with priority from partial instances not
%%% rejected by early priority test
%%% don't perform early tests on unlinked partial instances
%%% performed early unit subsumption test in get_hm_nucleus
%%% performed partial instance check in get_hm_nucleus
%%% no longer erased partial instances for each nucleus
%%% fixed electron instance check so it doesn't erase and assert lit_G while
%%% backtracking over lit_G
%%% version 2.05.5
%%% added equational rewriting
%%% don't erase clauses when erasing large rewrite rules
%%% version 2.05.6
%%% changed early unit subsumption to equality early unit subsumption
%%% added new early unit subsumption
%%% version 2.05.7
%%% ehanced equality early unit subsumption test
%%% don't hyper-link unit nuclei
%%% version 2.06.0
%%% added bug fixes from Shie-Jue
%%% added early check for unit conflict
%%% version 2.06.1
%%% fixed bug in hm_literal which sometimes erronously failed to link
%%% fully sort nuclei before hyper-linking
%%% version 2.06.2
%%% added fast_priority_update
%%% added duplicate_partial_instance_test
%%% check for unit conflict in hyper when sliding priority not specified
%%%
%%% hm_round hyper-matches the input clauses one round,
%%% and generates new clauses. These new clauses are not variant
%%% to each other, nor variant to any clause in the input clauses.
%%%
%%% The strategy here is bottom-up strategy.
%%% The idea is we find the first mate for the first literal, then
%%% find the first mate for the second literal, etc., until we find
%%% the first mate for the last literal. Then we backtrack for the
%%% last literal and find the second mate for the last literal, and
%%% then the last mate for the last literal. Then we backtrack to find
%%% the second mate for the next to last literal, and so forth, until
%%% we find the last mate for the first literal.
%%%
%%% The disadvantage for this is we can't delete duplicates for the
%%% intermediate hyper-matches. The advanteage for this strategy is that
%%% we don't need to store the intermediate hyper-matches.
%%%
%%% Some comments:
%%% (A)
%%% supported clause not implies new clause
%%% new clause implies supported clause in some strategy
%%% distance 0 clause implies supported clause
%%% distance 0 clause not implies new clause
%%% supported clause not implies distance 0 clause
%%% distance 0 clause iff supported input clause or its hyper-matches
%%% distance 0 clause and its hyper-matches implies supported clause
%%% (B)
%%% The calculation of distance should be done properly:
%%% 1. no same literal connects two edges in a path
%%% This requirement is not enforced for user support.
%%% 2. calculate three distances at the same time
%%% a. maximum forward distance for negative literals.
%%% b. maximum backward distance for positive literals.
%%% c. minimum user distance for user supported literals.
%%%
%%% Checking the number of distinct variales in a clause:
%%% If a hyper-match has more distichnct variables than constants in the
%%% constant list, then print out error message, ignore the hyper-
%%% match, and go ahead the proof.
%%%
%%% We keep three kinds of clauses. sent_C is the nuclei. sent_T are the
%%% hyper-matches which are duplicates to sent_C. sent_HM are hyper-matches
%%% which are not duplicates to sent_C.
%%% 1. take one sent_C.
%%% 2. Check a hyper-match against sent_HM, sent_T, sent_C.
%%% 3. If the hyper-match has no duplicates from neither source, then
%%% it is asserted as sent_HM. Increase the hyper-match number
%%% count.
%%% 4. If the hyper-match has a duplicate in sent_HM:
%%% a. If the clause information of the hyper-match is contained in
%%% those of the duplicate, do nothing.
%%% b. If not, then retract the duplicate, and assert a clause sent_HM
%%% with updated clause information.
%%% 5. If the hyper-match has a duplicate in sent_T:
%%% a. If the clause information of the hyper-match is contained in
%%% those of the duplicate, do nothing.
%%% b. If not, then retract the duplicate, and assert a clause sent_T
%%% with updated clause information.
%%% 6. If the hyper-match has a duplicate in sent_C, assert it as sent_T.
%%% 7. do throw-away strategy on sent_C.
%%% 8. Merge sent_T into sent_C and remove duplicates.
%%% 9. rename sent_HM to sent_C.
%%%
%%% Since we use contradiction checking in the prover, otherwise it is not
%%% complete, the following facts hold:
%%% 1. A nucelus has no unit mates in UR.
%%% 2. A unit nucleus has no unit mates in U,B,and F.
%%%
%%% Unit deletion: If a nucleus literal has a mate from a unit clause,
%%% then we won't record this literal in database with the instance.
%%% Empty hyper-match detection: The hyper-matching stops whenever an
%%% empty hyper-match is generated.
%%%
%%% Time control: Before we hyper-match a nucleus, we check if the time
%%% is overflowed. If so, stop the hyper-matching and do the other
%%% stages with the hyper-matches obtained so far.
%%%
%%% Shorter nucleus first serve: In order to reduce the number of assertions
%%% and deletions with sliding priority, we starts with the shorter
%%% nuclei to do hyper-matching.
%%%
%%% Add an option, ground_hyper_match, to accept ground hyper matches.
%%% If ground_hyper_match is specified, then
%%% we don't throw away nucleus
%%% we don't accept non-ground hyper-matches.
%%%
%%% Don't count ground literals when considering literal bounds.
%%% We check this after duplicate checking.
%%%
%%% Match ground literals first.
%%%
%%% The order of match is determined by the number of non-ground literals
%%% in a nucleus, not the number of literals any more, since ground
%%% literals do not backtrack.
%%% So we change data structure to have a field recording the number
%%% of non-ground literals in a clause.
%%%
hm_round :-
not(not(hm_round_fail)),
!.
hm_round_fail :-
cputime(TT1),
hm_round0,
cputime(TT2),
TT3 is TT2 - TT1,
update_hypermatch_time(TT3),
write_line(5,'Hyper-linking(s): ',TT3),
!.
%%% We record the time spent in hyper-matching just done. This time is
%%% used for controlling the following small proof checking.
update_hypermatch_time(TT3) :-
abolish(last_hypermatch_time,1),
assert(last_hypermatch_time(TT3)).
%%% 1. calculate the non-duplicate literal list.
%%% 2. obtain two literal lists: one is the list of supported literals
%%% and the other one is the whole list itself.
%%% 3. do hyper-matching one nucleus at a time.
%%% 4. update the clauses in the database.
hm_round0 :-
set_counter(counter1,0),
set_counter(counter2,0),
set_counter(counter3,0),
set_counter(counter4,0),
litsall_hm,
supported_mates,
sort_lits,
print_litsall,
bagof1(RSLit,(US,LBYS,LSS,LRS)^clause(lit_S(US,LBYS,LSS,LRS),
true,RSLit),RSLists),
bagof1(RGLit,(UG,LBYG,LSG,LRG)^clause(lit_G(UG,LBYG,LSG,LRG),
true,RGLit),RGLists),
hm_round1(RSLists,RGLists),
physically_erase(sent_C),
abolish(lit_S,4),
abolish(lit_G,4),
abolish(part_inst,4),
not(not(update_sentC)),
counter(counter1,Counter1),
write_line(10,'Early tautology: ',Counter1),
counter(counter2,Counter2),
write_line(10,'Duplicate Partial Instances: ',Counter2),
counter(counter3,Counter3),
write_line(10,'Early Unit Subsumption: ',Counter3),
counter(counter4,Counter4),
write_line(10,'Equality Early Unit Subsumption: ',Counter4),
!.
%%% sort the literals.
sort_lits :-
sort_lit_G,
sort_lit_S,
!.
sort_lit_G :-
bagof1([G1,G2,G3,G4],lit_G(G1,G2,G3,G4),GLits1),
abolish(lit_G,4),
sort_lit_G_1(GLits1,GLits2),
sort(GLits2,GLits3),
sort_lit_G_3(GLits3),
!.
sort_lit_G_1([],[]).
sort_lit_G_1([[G1,G2,G3,G4]|GLits1],[{S,Lg,[G1,G2,G3,G4]}|GLits2]) :-
G2=..[_,L,V1,V2,_],
not(not(sort_lit_G_2(L,V1,V2))),
retract(slG_temp1(S)),
retract(slG_temp2(Lg)),
!,
sort_lit_G_1(GLits1,GLits2).
sort_lit_G_2(L,V,V) :-
literal_size(L,S),
assert(slG_temp1(S)),
ground(L,Lg,_,_),
assert(slG_temp2(Lg)).
sort_lit_G_3([]).
sort_lit_G_3([{_,_,[G1,G2,G3,G4]}|GLits]) :-
assertz(lit_G(G1,G2,G3,G4)),
!,
sort_lit_G_3(GLits).
sort_lit_S :-
bagof1([S1,S2,S3,S4],lit_S(S1,S2,S3,S4),SLits1),
abolish(lit_S,4),
sort_lit_S_1(SLits1,SLits2),
sort(SLits2,SLits3),
sort_lit_S_3(SLits3),
!.
sort_lit_S_1([],[]).
sort_lit_S_1([[S1,S2,S3,S4]|SLits1],[{S,Lg,[S1,S2,S3,S4]}|SLits2]) :-
S2=..[_,L,V1,V2,_],
not(not(sort_lit_S_2(L,V1,V2))),
retract(slS_temp1(S)),
retract(slS_temp2(Lg)),
!,
sort_lit_S_1(SLits1,SLits2).
sort_lit_S_2(L,V,V) :-
literal_size(L,S),
assert(slS_temp1(S)),
ground(L,Lg,_,_),
assert(slS_temp2(Lg)).
sort_lit_S_3([]).
sort_lit_S_3([{_,_,[S1,S2,S3,S4]}|SLits]) :-
assertz(lit_S(S1,S2,S3,S4)),
!,
sort_lit_S_3(SLits).
%%% hyper-matching one clause each time.
%%% starting with the smallest clauses
hm_round1(RSLists,RGLists) :-
get_hm_nucleus(C,RefNucl),
hm_clause(C,RefNucl,RSLists,RGLists),
check_hm_stop,
!.
hm_round1(_,_).
%%% Stop if an empty hyper-match is generated or time overflows.
check_hm_stop :-
prove_result(unsatisfiable), !.
check_hm_stop :-
is_time_overflow.
%%% get a nucleus in order of number of literals.
get_hm_nucleus(C,RefNucl) :-
bagof1([N,S,Cg]-Ref,get_hm_nucleus_1(N,S,Cg,Ref),Nuclei1),
keysort(Nuclei1,Nuclei2),
member([_,_,_]-RefNucl,Nuclei2),
not(logically_erased(sent_C,RefNucl)),
clause(sent_C(C),true,RefNucl),
C=cl(_,_,By,_,Sp,Ds,_,_,Pr),
not(not(get_hm_nucleus_3(By))).
get_hm_nucleus_1(N,S,C4,Ref) :-
clause(sent_C(cl(S,N,by([L1,L2|C1],V,V,_,_),_,_,_,_,_,_)),true,Ref),
get_hm_nucleus_2([L1,L2|C1],C2),
ground(C2,C3,_,_),
keysort(C3,C4).
get_hm_nucleus_2([],[]) :- !.
get_hm_nucleus_2([L1|C1],[L2-dummy|C2]) :-
(L1=not(L1n) -> (
L2=L1n
); (
L2=L1
)),
get_hm_nucleus_2(C1,C2).
get_hm_nucleus_3(by(Cn1,V1,V1,_,_)) :-
create_LnkLits(Cn1,LnkLits),
hm_literal_14(Cn1,LnkLits),
!.
%%% Hyper-match the nucleus.
%%% If UR round, do nothing if
%%% 1. the nucleus is not original input clause.
%%% 2. the nucleus is original input clause, but unit.
hm_clause(cl(_,_,by(Cn1,_,_,_,_),0,CS1,_,CT1,_,_),RefNucl,_,_) :-
current_support(sup(_,_,_,1)),
check_throw_nucleus(0,CT1,Cn1,CS1,RefNucl),
!, fail.
hm_clause(cl(_,_,by([_],_,_,_,_),1,_,_,_,_,_),_,_,_) :-
current_support(sup(_,_,_,1)),
!, fail.
hm_clause(cl(CSize1,_,by(Cn1,V11,V11,V1,W1),CI1,CS1,CR1,CT1,CF1,CP1),
RefNucl,RSLists,RGLists) :-
print_nucleus(Cn1,V1,CS1,CR1,CF1),
decide_unit(Cn1,U),
check_throw_nucleus(CI1,CT1,Cn1,CS1,RefNucl),
negate_clause(Cn1,NCn1),
!,
hm_clause1(RefNucl,U,CF1,Cn1,NCn1,W1,CS1,CR1,RSLists,RGLists,
CF2,Cn2a,W2a,DFlag,CS2,CR2),
rewrite_clause(Cn2a,CS2,CR2,1,Cn2,_),
hm_clause2(Cn2,W2a,W2),
hm_clause3(RefNucl,U,CSize1,CP1,CF2,Cn2,V1,W2,DFlag,CS2,CR2).
hm_clause2(_,W2,W2) :-
not(rwr(_,_,_,_)),
!.
hm_clause2(Cn2,_,W2) :-
vars_literals(Cn2,W2),
!.
hm_clause3(RefNucl,U,CSize1,CP1,CF2,Cn2,V1,W2,DFlag,CS2,CR2) :-
process_HM(RefNucl,U,CSize1,CP1,CF2,Cn2,V1,W2,DFlag,CS2,CR2),
check_empty_hm(Cn2).
hm_clause3(_,_,_,_,_,_,_,_,_,_,_) :-
is_time_overflow.
%%% If an empty hyper-match is generated, assert information into database.
check_empty_hm([]) :-
assert_tryresult('unsatisfiable'),
assert_prooftype('HM'), !.
check_empty_hm(_).
%%% If sliding priority is used.
process_HM(RefNucl,U,CSize1,CP1,F2,Cn2,V1,W2,DFlag,CS2,CR2) :-
slidepriority,
!, prio_test(U,CP1,Cn2,DFlag,V1,CS2,CR2,CP2),
calculate_new_size(U,CSize1,Cn2,DFlag,V1,CSize2),
make_varstail(U,V1,W2,V2),
!, check_numbervars(V2,'Number of variables overflows in instances !'),
!, totalhm_test(RefNucl,U,CSize2,CP2,F2,Cn2,V2,W2,CS2,CR2), !.
%%% If fixed priority is used.
process_HM(RefNucl,U,CSize1,CP1,F2,Cn2,V1,W2,DFlag,CS2,CR2) :-
fixed_priority,
!,
prio_test(U,CP1,Cn2,Dflag,V1,CS2,CR2,CP2),
calculate_new_size(U,CSize1,Cn2,DFlag,V1,CSize2),
make_varstail(U,V1,W2,V2),
!, check_numbervars(V2,'Number of variables overflows in instances !'),
!, noslide_update_HM(RefNucl,U,CSize2,CP1,F2,Cn2,V2,W2,CS2,CR2), !.
%%% If no fixed or sliding priority.
process_HM(RefNucl,U,CSize1,CP1,F2,Cn2,V1,W2,DFlag,CS2,CR2) :-
calculate_new_size(U,CSize1,Cn2,DFlag,V1,CSize2),
make_varstail(U,V1,W2,V2),
!, check_numbervars(V2,'Number of variables overflows in instances !'),
!, noslide_update_HM(RefNucl,U,CSize2,CP1,F2,Cn2,V2,W2,CS2,CR2), !.
%%% N1 is used for recording if a literal in a hyper-match is unit-deleted
%%% or not. If it is unit deleted, the correponding element at appropriate
%%% position is 1, otherwise it is 0.
%%% CR1 is separated into two sublists: Ord1 and Ord2. Ord1 are the literals
%%% to be matched by supported mates. Ord2 are the literals to be
%%% matched by any mates. We matched Ord1 first, then Ord2 for efficiency
%%% purpose.
hm_clause1(RefNucl,U,F1,Cn1,NCn1,W1,CS1,CR1,RSLists,RGLists,
F2,Cn2,W2,DFlag,CS2,CR2) :-
clause_part2(CS1,CR1,CSM1,CRM1),
matord(NCn1,Ord1,Ord2,W1,WO1,WO2,N1,NOrd1,NOrd2),
!,
hm_clause1_2(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,RefNucl,U,
RSLists,RGLists,CSM1,CRM1,CS2,CRM2,Cn1),
hm_clause1_3(N1,F1,Cn1,W1,CR1,CS2,CRM2,F2,Cn2,W2,DFlag,CR2).
%%% If the current round is user support round.
hm_clause1_2(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
current_support(sup(1,0,0,0)),
!,
hm_user(Ord1,WO1,NOrd1,RefNucl,U,RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1).
%%% If the current round is UR support round.
hm_clause1_2(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
current_support(sup(_,_,_,1)),
!,
hm_ur(Ord1,WO1,NOrd1,RefNucl,U,RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1).
%%% Otherwise.
hm_clause1_2(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
hm_bf(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,RefNucl,U,RSLists,RGLists,
CS1,CR1,CS2,CR2,Cn1).
%%% For UR, we take one literal unmatched, then match the other literals
%%% with unit clauses.
%%% In order to match ground literals first, we have to change the algorithm.
%%% hm_ur([Ln1|Lns1],[0|Ts1],RefNucl,U,RSLists,RGLists,CS1,CR1,CS2,CR2) :-
%%% hm_literals(Lns1,U,RefNucl,CS1,CR1,0,RSLists,Ts1,CS2,CR2).
%%% hm_ur([Ln1|[Ln2|Lns1]],[T1|Ts1],RefNucl,U,
%%% RSLists,RGLists,CS1,CR1,CS2,CR2) :-
%%% hm_literal(U,RefNucl,Ln1,CS1,CR1,0,RSLists,T1,CSM,CRM),
%%% hm_ur([Ln2|Lns1],Ts1,RefNucl,U,RSLists,RGLists,CSM,CRM,CS2,CR2).
%%%
hm_ur([Ln1|Lns1],[W1|Ws1],[0|Ts1],RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
create_LnkLits(Cn1,LnkLits),
update_LnkLits(Cn1,Ln1,LnkLits,0),
hm_literals(Lns1,Ws1,U,RefNucl,CS1,CR1,0,RSLists,Ts1,CS2,CR2,Cn1,
LnkLits).
hm_ur([Ln1|[Ln2|Lns1]],[W1|Ws1],[T1|Ts1],RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
hm_ur_1([Ln2|Lns1],Ws1,Ts1,RefNucl,U, RSLists,RGLists,CS1,CR1,
[Ln1|KL1],[W1|KW1],[T1|KT1],KL1,KW1,KT1,CS2,CR2,Cn1).
hm_ur_1([Ln1|Lns1],[W1|Ws1],[0|Ts1],RefNucl,U, RSLists,RGLists,CS1,CR1,
KL1,KW1,KT1,Lns1,Ws1,Ts1,CS2,CR2,Cn1) :-
create_LnkLits(Cn1,LnkLits),
update_LnkLits(Cn1,Ln1,LnkLits,0),
hm_literals(KL1,KW1,U,RefNucl,CS1,CR1,0,RSLists,KT1,CS2,CR2,Cn1,
LnkLits).
hm_ur_1([Ln1|[Ln2|Lns1]],[W1|Ws1],[T1|Ts1],RefNucl,U, RSLists,RGLists,
CS1,CR1,KL1,KW1,KT1,[Ln1|KL2],[W1|KW2],[T1|KT2],CS2,CR2,Cn1) :-
hm_ur_1([Ln2|Lns1],Ws1,Ts1,RefNucl,U, RSLists,RGLists,
CS1,CR1,KL1,KW1,KT1,KL2,KW2,KT2,CS2,CR2,Cn1).
%%% For user support, we match one literal with user supported mates, then
%%% match the other literals with any mates.
%%% In order to match ground literals first, we have to change the algorithm.
%%% hm_user([Ln1|Lns1],[T1|Ts1],RefNucl,U,RSLists,RGLists,CS1,CR1,CS2,CR2) :-
%%% hm_literal(U,RefNucl,Ln1,CS1,CR1,0,RSLists,T1,CSM,CRM),
%%% hm_literals(Lns1,U,RefNucl,CSM,CRM,1,RGLists,Ts1,CS2,CR2).
%%% hm_user([Ln1|[Ln2|Lns1]],[T1|Ts1],RefNucl,U,
%%% RSLists,RGLists,CS1,CR1,CS2,CR2) :-
%%% hm_literal(U,RefNucl,Ln1,CS1,CR1,1,RGLists,T1,CSM,CRM),
%%% hm_user([Ln2|Lns1],Ts1,RefNucl,U,RSLists,RGLists,CSM,CRM,CS2,CR2).
%%%
hm_user([Ln1|Lns1],[W1|Ws1],[T1|Ts1],RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
create_LnkLits(Cn1,LnkLits),
hm_user_literal_U(W1,Ws1,U,RefNucl,Ln1,CS1,CR1,0,RSLists,T1,Ws2,
CSM,CRM,Cn1,Lns1,LnkLits),
hm_literals(Lns1,Ws2,U,RefNucl,CSM,CRM,1,RGLists,Ts11,CS2,CR2,Cn1,
LnkLits).
hm_user([Ln1|[Ln2|Lns1]],[W1|Ws1],[T1|Ts1],RefNucl,U,
RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
hm_user_1([Ln2|Lns1],Ws1,Ts1,RefNucl,U,RSLists,RGLists,CS1,CR1,
[Ln1|KL1],[W1|KW1],[T1|KT1],KL1,KW1,KT1,CS2,CR2,Cn1).
hm_user_1([Ln1|Lns1],[W1|Ws1],[T1|Ts1],RefNucl,U, RSLists,RGLists,CS1,CR1,
KL1,KW1,KT1,Lns1,Ws1,Ts1,CS2,CR2,Cn1) :-
create_LnkLits(Cn1,LnkLits),
hm_user_literal_U(W1,Ws1,U,RefNucl,Ln1,CS1,CR1,0,RSLists,T1,Ws2,
CSM,CRM,Cn1,Lns1,LnkLits),
hm_literals(KL1,KW1,U,RefNucl,CSM,CRM,1,RGLists,KT1,CS2,CR2,Cn1,
LnkLits).
hm_user_1([Ln1|[Ln2|Lns1]],[W1|Ws1],[T1|Ts1],RefNucl,U,RSLists,RGLists,
CS1,CR1,KL1,KW1,KT1,[Ln1|KL2],[W1|KW2],[T1|KT2],CS2,CR2,Cn1) :-
hm_user_1([Ln2|Lns1],Ws1,Ts1,RefNucl,U,RSLists,RGLists,
CS1,CR1,KL1,KW1,KT1,KL2,KW2,KT2,CS2,CR2,Cn1).
hm_user_literal_U(W1,Ws1,U,RefNucl,Ln1,CS1,CR1,Type,RSLists,T1,Ws1,
CS2,CR2,Cn1,Ls1,LnkLits) :-
var(W1),
!, hm_literal(U,RefNucl,Ln1,CS1,CR1,Type,RSLists,T1,CS2,CR2,Cn1,
LnkLits),
!.
hm_user_literal_U(_,Ws1,U,RefNucl,Ln1,CS1,CR1,Type,RSLists,T1,Ws2,
CS2,CR2,Cn1,Ls1,LnkLits) :-
hm_literal(U,RefNucl,Ln1,CS1,CR1,Type,RSLists,T1,CS2,CR2,Cn1,LnkLits),
w1_w2(Ws1,Ws2).
%%% For forward support, we match all negative literals with forward
%%% supported mates, then mathc the other literals with any mates.
%%% For backward support, we match all positive literals with backward
%%% supported mates, then mathc the other literals with any mates.
hm_bf(Ord1,Ord2,WO1,WO2,NOrd1,NOrd2,
RefNucl,U,RSLists,RGLists,CS1,CR1,CS2,CR2,Cn1) :-
create_LnkLits(Cn1,LnkLits),
hm_literals(Ord1,WO1,U,RefNucl,CS1,CR1,0,RSLists,NOrd1,CSM,CRM,Cn1,
LnkLits),
w1_w2(WO2,WO3),
hm_literals(Ord2,WO3,U,RefNucl,CSM,CRM,1,RGLists,NOrd2,CS2,CR2,Cn1,
LnkLits).
%%% Check if it is user supported if it is required so.
%%% Delete all literals that are unit deleted, i.e., the litearls
%%% whose corresponding entries in N1 are 1s.
%%% Delete any duplicate literals in the hyper-match.
%%% Check literal bound.
%%% Adjust user distance.
%%% Check relevance bound.
hm_clause1_3(N1,F1,Cn1,W1,CR1,CS2,CRM2,F2,Cn2,W2,DFlag,CR2) :-
check_supp_u(CS2),
literals_remain_3(N1,Cn1,W1,F1,CnM,WM,FM,DFlag),
delete_replicate_literals_3(CnM,WM,FM,Cn2,W2,F2),
adjust_userdist(CRM2,CR1,CR2),
!, check_rel_clause(CR1,Cn2,CR2), !.
%%% LITSALL_HM ROUTINES:
%%%
%%% The format for literal is:
%%% lit_G(U,lby(Ln1,V21,V22,Wn2),CS1,CR1)
%%% U = 1 if the literal comes from a unit clause.
%%% U = 0 if the literal comes from a non-unit clause.
%%%
%%% The idea is that we collect a set of literals. No repetition of the
%%% literals are allowed. If two literals coming from different sources
%%% and have different S and R, then we update S and R to reflect the
%%% least distance to the support sets for calculating relevance and the
%%% most possibility to be supported for hyper-matching.
%%%
%%% Comments:
%%% The following procedure is used if unit_resolution is specified.
%%% If a literal comes from a unit clause, it is inserted into the
%%% database directly without duplicate checking because
%%% we know that there should be no duplicates after the
%%% unit subsumption and unit simplification.
%%% If a literal comes from a non-unit clause, we don't need to
%%% check the duplicates against the unit-clause literals
%%% because of the reason stated above. However, we need
%%% to check duplicates against the other non-unit-clause
%%% literals.
%%% For efficiency, we do for non-unit clauses first, then for unit clauses.
%%%
%%% Instance deletion: If instance deletion is specified, then we do the
%%% following operation. If a literal L1 is an instance of L2, and
%%% L1 is not a unit clause, then delete L1.
%%%
litsall_hm :-
not(not(litsall_hm_1)),
!.
litsall_hm_1 :-
current_support(sup(_,_,_,1)),
litsall_hm_ur, !.
litsall_hm_1 :-
litsall_hm_ubf, !,
instdel_lits, !.
%%% If UR is specified, then we only have to find the literals from unit
%%% clauses.
%%% Furthermore, we make the literal list as lit_S directly.
litsall_hm_ur :-
sent_C(cl(_,_,by([Ln1],V11,V12,_,[Wn1]),_,CS1,CR1,_,_,_)),
assertz(lit_S(1,lby(Ln1,V11,V12,Wn1),CS1,CR1)),
fail.
litsall_hm_ur.
%%% If the round is not UR round.
%%% litsall_hm_ubf1(T1,T2):
%%% T1 means the existing lit_G(T1,...) in database.
%%% T2 means the coming lit_G(T2,...).
litsall_hm_ubf :-
litsall_hm_ubf1(0,0),
litsall_hm_ubf2, !.
%%% Find literals for non-unit clauses.
litsall_hm_ubf1(T1,T2) :-
sent_C(cl(_,_,by([Ln1,Ln2|Lns1],V11,V12,_,W1),_,CS1,CR1,_,_,_)),
litsall_hm_ubf1([Ln1,Ln2|Lns1],V11,V12,W1,CS1,CR1,T1,T2),
fail.
litsall_hm_ubf1(_,_).
%%% Process one literal each time.
litsall_hm_ubf1([],_,_,_,_,_,_,_).
litsall_hm_ubf1([Ln1|Lns1],V11,V12,[Wn1|Wns1],CS1,CR1,T1,T2) :-
\+ lit_copy(Ln1,V11,V12,Wn1,CS1,CR1,T1,T2),
assertz(lit_G(T2,lby(Ln1,V11,V12,Wn1),CS1,CR1)),
!,
litsall_hm_ubf1(Lns1,V11,V12,Wns1,CS1,CR1,T1,T2).
litsall_hm_ubf1([Ln1|Lns1],V11,V12,[Wn1|Wns1],CS1,CR1,T1,T2) :-
!, % green cut.
litsall_hm_ubf1(Lns1,V11,V12,Wns1,CS1,CR1,T1,T2).
%%% Check duplicates.
lit_copy(Ln1,V11,V11,Wn1,CS1,CR1,T1,T2) :-
const_list(Wn1),
lit_G(T1,lby(Ln1,V21,V21,Wn2),CS2,CR2),
const_list(Wn2),
binary_max_ind(T1,T2,T3,Up),
max_CS_ind(CS2,CS1,CS3,Up),
min_CR_ind(CR2,CR1,CR3,Up),
lit_copy_1(Up,CS3,CR3,T3,Ln1).
lit_copy_1(n,_,_,_,_) :- !.
lit_copy_1(_,CS3,CR3,T3,Ln1) :-
clause(lit_G(_,lby(Ln1,V21,V21,Wn2),_,_),true,Ref2),
const_list(Wn2),
clause(lit_G(_,LBY_2,_,_),true,Ref2),
erase(Ref2),
assertz(lit_G(T3,LBY_2,CS3,CR3)), !.
%%% Find literals of unit clauses.
%%% If unit resolution is specified, we don't need to check the duplicates
%%% for the literals from unit clauses.
litsall_hm_ubf2 :-
sent_C(cl(_,_,by([Ln1],V11,V12,_,[Wn1]),_,CS1,CR1,_,_,_)),
assertz(lit_G(1,lby(Ln1,V11,V12,Wn1),CS1,CR1)),
fail.
litsall_hm_ubf2.
%%% Delete literal instances.
%%% To check if a literal D is an instance of C, there are 4 cases:
%%% 1. D unit, C unit. Impossible because of unit subsumption.
%%% 2. D unit, C not unit. Do not delete D.
%%% 3. D not unit, C unit. Impossible because of unit subsumption.
%%% 4. D not unit, C not unit. Only this case has to be considered.
instdel_lits :-
\+ delete_all_instances,
\+ delete_nf_instances, !.
instdel_lits :-
abolish(lit_G1,3),
instdel_lits_1,
abolish(lit_G1,3).
instdel_lits_1 :-
clause(lit_G(0,lby(Ln1,V11,V11,Wn1),_,_),true,Ref),
get_lit_G_data(Ref,CS1,CR1),
const_list(Wn1),
retract_lit_G(LBY2),
instdel_lits_ckinst(Ln1,CS1,CR1,lit_S(0,LBY2,CS1,CR1)), fail.
instdel_lits_1 :-
retract(lit_S(T,LBY,S,R)),
assertz(lit_G(T,LBY,S,R)),
fail.
instdel_lits_1.
retract_lit_G(LBY2) :-
retract(lit_G(0,LBY2,_,_)), !.
instdel_lits_ckinst(Ln1,CS1,CR1,L1) :-
delete_all_instances,
instdel_lits_ckinst_all(Ln1,CS1,CR1,L1), !.
instdel_lits_ckinst(Ln1,CS1,CR1,L1) :-
delete_nf_instances,
instdel_lits_ckinst_nf(Ln1,CS1,CR1,L1), !.
instdel_lits_ckinst_all(Ln1,CS1,CR1,_) :-
instdel_lits_lit_inst(Ln1,CS1,CR1).
instdel_lits_ckinst_all(_,_,_,L1) :-
assertz(L1).
instdel_lits_ckinst_nf(Ln1,sp(S11,S12,0),CR1,_) :-
instdel_lits_lit_inst(Ln1,sp(S11,S12,0),CR1).
instdel_lits_ckinst_nf(_,_,_,L1) :-
assertz(L1).
instdel_lits_lit_inst(Ln1,CS1,CR1) :-
clause(lit_G(0,lby(Ln1,V21,V21,_),_,_),true,Ref2),
get_lit_G_data(Ref2,CS2,CR2),
instdel_lits_lit_inst_2('G',CS1,CR1,Ln1,CS2,CR2).
instdel_lits_lit_inst(Ln1,CS1,CR1) :-
lit_S(0,lby(Ln1,V21,V21,_),CS2,CR2),
instdel_lits_lit_inst_2('S',CS1,CR1,Ln1,CS2,CR2).
instdel_lits_lit_inst_2(_,sp(1,_,_),_,_,sp(0,_,_),_) :- !, fail.
instdel_lits_lit_inst_2(_,sp(0,1,_),_,_,sp(_,0,_),_) :- !, fail.
instdel_lits_lit_inst_2(T,CS1,CR1,Ln1,CS2,CR2) :-
max_CS_ind(CS2,CS1,CS3,Up),
min_CR_ind(CR2,CR1,CR3,Up),
instdel_lits_lit_inst_1(T,Up,Ln1,CS3,CR3).
instdel_lits_lit_inst_1(_,n,_,_,_) :- !.
instdel_lits_lit_inst_1('G',_,Ln1,CS3,CR3) :-
clause(lit_G(0,lby(Ln1,V21,V21,_),_,_),true,Ref2),
update_lit_G_data(Ref2,CS3,CR3).
instdel_lits_lit_inst_1('S',_,Ln1,CS3,CR3) :-
clause(lit_S(0,lby(Ln1,V21,V21,_),_,_),true,Ref2),
clause(lit_S(0,LBY2,_,_),true,Ref2),
erase(Ref2),
assertz(lit_S(0,LBY2,CS3,CR3)).
update_lit_G_data(Ref,CS,CR) :-
retract(lit_G1(Ref,_,_)),
assertz(lit_G1(Ref,CS,CR)),
!.
update_lit_G_data(Ref,CS,CR) :-
assertz(lit_G1(Ref,CS,CR)),
!.
get_lit_G_data(Ref,CS,CR) :-
lit_G1(Ref,CS,CR),
!.
get_lit_G_data(Ref,CS,CR) :-
clause(lit_G(_,_,CS,CR),true,Ref),
!.
%%% SUPPORTED_MATES
%%%
%%% Find out supported mates.
%%% If UR then do nothing.
supported_mates :-
current_support(sup(_,_,_,1)), !.
supported_mates :-
current_support(sup(1,0,0,0)),
supported_mates_u, !.
supported_mates :-
current_support(sup(_,1,0,_)),
supported_mates_b, !.
supported_mates :-
current_support(sup(_,0,1,_)),
supported_mates_f, !.
supported_mates :-
current_support(sup(_,1,1,_)),
supported_mates_bf.
%%% Find out user supported literals.
supported_mates_u :-
lit_G(UG,P,sp(1,S2,S3),R),
assertz(lit_S(UG,P,sp(1,S2,S3),R)),
fail.
supported_mates_u.
%%% Find out backward supported negative literals.
supported_mates_b :-
lit_G(UG,lby(P,V11,V12,W1),sp(S1,1,S3),R),
negative_lit(P),
assertz(lit_S(UG,lby(P,V11,V12,W1),sp(S1,1,S3),R)),
fail.
supported_mates_b.
%%% Find out forward supported positive literals.
supported_mates_f :-
lit_G(UG,lby(P,V11,V12,W1),sp(S1,S2,1),R),
\+ negative_lit(P),
assertz(lit_S(UG,lby(P,V11,V12,W1),sp(S1,S2,1),R)),
fail.
supported_mates_f.
%%% Find out backward supported negative and forward supported
%%% positive literals.
supported_mates_bf :-
supported_mates_b,
leave_mates_f.
leave_mates_f :-
clause(lit_G(_,lby(P,_,_,_),sp(_,_,S3),_),true,Ref1),
\+ positive_f_mate(P,S3),
erase(Ref1),
fail.
leave_mates_f.
positive_f_mate(P,1) :-
\+ negative_lit(P).
%%% UPDATE_SENTC
%%%
%%% 1. duplicate checking
%%% 2. copying sent_HM.
%%%
update_sentC :-
const_list(Clist),
update_sentC_1(Clist),
sentHM_to_sentC_a.
%%% Pick one sent_T at a time.
update_sentC_1(Clist) :-
retract(sent_T(C1)),
update_sentC_3(C1,Clist),
fail.
update_sentC_1(_).
%%% Duplicate check against sent_C.
update_sentC_3(cl(CSize1,CN1,by(Cn1,V11,V11,Clist,_),_,CS1,CR1,
CT1,F1,pr(_,_,PL1,_,PX1)),Clist) :-
sent_C(cl(CSize1,CN1,by(Cn1,V21,V21,Clist,_),CI2,CS2,CR2,CT2,F2,
pr(_,_,PL2,_,PX2))),
min_ind(PL2,PL1,PL3,Up),
min_ind(PX2,PX1,PX3,Up),
binary_max_ind(CT2,CT1,CT3,Up),
min_Flags_ind(F2,F1,F3,Up),
max_CS_ind(CS2,CS1,CS3,Up),
min_CR_ind(CR2,CR1,CR3,Up),
update_sentC_31(Up,Cn1,Clist,PL3,PX3,F3,CS3,CR3,CI2,CT3), !.
update_sentC_3(C1,_) :-
asserta(sent_C(C1)), !.
%%% If the information is not changed, do nothing.
update_sentC_31(n,_,_,_,_,_,_,_,_,_).
update_sentC_31(_,Cn1,Clist,PL3,PX3,F3,CS3,CR3,CI2,CT3) :-
clause(sent_C(cl(_,_,by(Cn1,V21,V21,Clist,_),_,_,_,_,_,_)),true,Ref2),
clause(sent_C(cl(CSize2,CN2,BY_2,_,_,_,_,_,pr(PS2,PD2,_,_,_))),
true,Ref2),
erase(Ref2),
priority_NewPR(CR3,PR3),
asserta(sent_C(cl(CSize2,CN2,BY_2,CI2,CS3,CR3,CT3,F3,
pr(PS2,PD2,PL3,PR3,PX3)))).
%%% FIXED and SLIDING PRIORITY
%%%
%%% priority test.
%%% Calculate priority for the hyper-match.
%%% Check if the priority computed is larger than the current priority
%%% bound.
prio_test(U,CP1,Cn2,DL,V1,CS2,CR2,CP2) :-
calculate_priority_HM(U,CP1,Cn2,DL,V1,CS2,CR2,CP2),
priority_bound(PrioBound),
!,
check_prioritybound(CP2,PrioBound).
%%% If the nucleus is unit clause and the hyper-match is not empty.
calculate_priority_HM(1,pr(PS1,PD1,_,_,PX1),[Ln2],_,_,CS2,CR2,
pr(PS1,PD1,PL2,PR2,PX2)) :-
not(rwr(_,_,_,_)),
literal_coef(LCoef),
relevance_coef(RCoef),
priority_PL(LCoef,[Ln2],CS2,PL2),
maximum(PX1,PL2,XX1),
priority_PR(RCoef,CR2,PR2),
maximum(XX1,PR2,PX2), !.
%%% If the nuclues if ground.
calculate_priority_HM(_,pr(PS1,PD1,_,_,PX1),Cn2,0,V1,CS2,CR2,
pr(PS1,PD1,PL2,PR2,PX2)) :-
var(V1),
not(rwr(_,_,_,_)),
literal_coef(LCoef),
relevance_coef(RCoef),
priority_PL(LCoef,Cn2,CS2,PL2),
maximum(PX1,PL2,XX1),
priority_PR(RCoef,CR2,PR2),
maximum(XX1,PR2,PX2), !.
%%% Otherwise.
calculate_priority_HM(_,_,Cn2,_,_,CS2,CR2,pr(PS,PD,PL,PR,P)) :-
depth_coef(DCoef),
size_coef(SCoef),
literal_coef(LCoef),
relevance_coef(RCoef),
priority_PS(SCoef,Cn2,PS),
priority_PD(DCoef,Cn2,PD),
priority_PL(LCoef,Cn2,CS2,PL),
priority_PR(RCoef,CR2,PR),
priority_clause(PS,PD,PL,PR,P), !.
%%% If the priority of the hyper-match M is larger than the current
%%% priority bound, discard M.
check_prioritybound(pr(_,_,_,_,P),PrioBound) :-
P =< PrioBound.
check_prioritybound(_,_) :-
assert_once(over_priohm), !, fail.
%%% If the hyper-match is a duplicate, do nothing.
totalhm_test(_,_,CSize2,CP2,F2,Cn2,V2,_,CS2,CR2) :-
update_HM(CSize2,CP2,F2,Cn2,V2,CS2,CR2), !.
%%% Check for unit conflict proof.
totalhm_test(_,_,_,_,_,Cn2,_,_,_,_) :-
(check_unit_conflict_C(Cn2); check_unit_conflict_HM(Cn2)),
!,
assert_tryresult('unsatisfiable'),
assert_prooftype('UC').
%%% If the hyper-match is not a duplicate, check the number of hyper-matches
%%% already in database.
totalhm_test(RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2) :-
prio_parameters(TotalHm,ExpectWU,TotalWU), !,
totalhm_test1(hm,RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2,
TotalHm,ExpectWU,TotalWU),
!.
%%% Obtain some information from database.
prio_parameters(TotalHm,ExpectWU,TotalWU) :-
total_numhm(TotalHm),
wu_bound(ExpectWU),
total_wu(TotalWU).
%%% Test if the total hyper-matches in the session exceeds the hyper-match
%%% bound.
%%% If the total hyper-matches doesn't exceed the hyper-match bound, then
%%% update counters and assert the hyper-match.
totalhm_test1(Type,RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2,
TotalHm_1,ExpectWU,TotalWU_1) :-
add_PT2(CP2,TotalWU_1,TotalWU_2),
TotalWU_2 =< ExpectWU,
TotalHm_2 is TotalHm_1 + 1,
update_numhm_wu(TotalHm_2,TotalWU_2),
update_priowu(CP2),
proc_C(U,RefNucl,Cn2,V2,W1,CN2,Cn3,V21,V22,V3,W2),
!, check_literalbound(Type,CN2,CS2),
print_HM(Cn2,V2,CS2,CR2,F2),
assert_an_HM(Type,CSize2,CN2,by(Cn3,V21,V22,V3,W2),CS2,CR2,F2,CP2), !.
%%% If the total hyper-matches exceeds the hyper-match bound, then
%%% find out the maximum priority in the hyper-matches.
totalhm_test1(Type,RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2,
TotalHm_1,ExpectWU,TotalWU_1) :-
max_priority(MaxPrio),
retract_priowu(pr(_,_,_,_MaxPrio),MaxNum,WUMaxPrio),
MaxPrioMinusOne is MaxPrio - 1,
update_priority_bound(MaxPrioMinusOne),
rmhm_prio(MaxPrio),
rmrwr_prio(MaxPrio),
rmpartinst_prio(MaxPrio),
totalhm_test2(Type,RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2,
TotalHm_1,TotalWU_1,MaxPrio,MaxNum,WUMaxPrio).
%%% Make 0 for hyper-match, and 1 for instance of replace rules.
assert_an_HM(hm,CSize2,CN2,BY2,CS2,CR2,F2,CP2) :-
asserta(sent_HM(cl(CSize2,CN2,BY2,0,CS2,CR2,0,F2,CP2))).
assert_an_HM(_,CSize2,CN2,BY2,CS2,CR2,F2,CP2) :-
asserta(sent_HM(cl(CSize2,CN2,BY2,0,CS2,CR2,1,F2,CP2))).
%%% Update total number of hyper-matches and work units.
update_numhm_wu(TotalHm_2,TotalWU_2) :-
retract(total_numhm(_)),
retract(total_wu(_)),
assert(total_numhm(TotalHm_2)),
assert(total_wu(TotalWU_2)).
%%% Update the number of hyper-matches with particular priority,
%%% the priority itself, and the work-units of the priority.
update_priowu(CP2) :-
retract_priowu(CP2,NumHm_1,WU_1),
add_PT2(CP2,WU_1,WU_2),
NumHm_2 is NumHm_1 + 1,
assert_priowu(CP2,NumHm_2,WU_2).
retract_priowu(pr(_,_,_,_,Prio),NumHm,WU) :-
retract(prio_wu(Prio,NumHm,WU)), !.
retract_priowu(_,0,0).
assert_priowu(pr(_,_,_,_,Prio),NewNumHm,NewWU) :-
assert(prio_wu(Prio,NewNumHm,NewWU)).
%%% Update current priority bound.
update_priority_bound(NewPr) :-
retract(priority_bound(Pr)),
assert(priority_bound(NewPr)).
%%% Find the maximum priority of non-input clauses.
max_priority(MaxPrio) :-
bagof1(P,(N1,N2)^prio_wu(P,N1,N2),Ps),
max_list(Ps,MaxPrio).
%%% If the priority is identical to the largest priority.
totalhm_test2(_,_,_,_,pr(_,_,_,_,MaxPrio),_,_,_,_,_,_,
TotalHm_1,TotalWU_1,MaxPrio,MaxNum,WUMaxPrio) :-
TotalHm_2 is TotalHm_1 - MaxNum,
TotalWU_2 is TotalWU_1 - WUMaxPrio,
update_numhm_wu(TotalHm_2,TotalWU_2), !.
%%% If the priority is not identical to the largest priority.
totalhm_test2(Type,RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2,
TotalHm_1,TotalWU_1,MaxPrio,MaxNum,WUMaxPrio) :-
TotalHm_2 is TotalHm_1 - MaxNum + 1,
YY is TotalWU_1 - WUMaxPrio,
add_PT2(CP2,YY,TotalWU_2),
update_numhm_wu(TotalHm_2,TotalWU_2),
update_priowu(CP2),
proc_C(U,RefNucl,Cn2,V2,W1,CN2,Cn3,V21,V22,V3,W2),
!, check_literalbound(Type,CN2,CS2),
print_HM(Cn2,V2,CS2,CR2,F2),
assert_an_HM(Type,CSize2,CN2,by(Cn3,V21,V22,V3,W2),CS2,CR2,F2,CP2), !.
add_PT2(pr(_,_,_,_,PT),Old,New) :-
New is Old + PT, !.
%%% Delete clauses having P too big and it is not an input clause.
rmhm_prio(P) :-
clause(sent_C(cl(_,_,by(C1,V1,V1,V2,_),0,_,_,_,_,pr(_,_,_,_,P))),true,
Cref),
not(logically_erased(sent_C,Cref)),
logically_erase(sent_C,Cref),
fail.
rmhm_prio(P) :-
clause(sent_HM(cl(_,_,by(C1,V1,V1,V2,_),0,_,_,_,_,pr(_,_,_,_,P))),true,
Cref),
erase(Cref),
fail.
rmhm_prio(P) :-
clause(sent_T(cl(_,_,by(C1,V1,V1,V2,_),0,_,_,_,_,pr(_,_,_,_,P))),true,
Cref),
erase(Cref),
fail.
rmhm_prio(_) :-
assert_once(over_priohm).
%%% Calculate size for hyper-match.
%%% Unit nucleus.
calculate_new_size(1,CSize1,[_],_,_,CSize1) :-
not(rwr(_,_,_,_)),
!.
%%% Empty hyper-match.
calculate_new_size(_,_,[],_,_,0) :- !.
%%% Ground nucleus and no literal deletion.
calculate_new_size(_,CSize1,_,0,V1,CSize1) :-
var(V1),
!.
%%% Otherwise.
calculate_new_size(_,_,Cn2,_,_,CSize2) :-
clause_size(Cn2,CSize2), !.
%%% Nucleus is unit.
proc_C(1,Ref,[_],_,_,CN3,Cn3,V31,V32,V3,W3) :-
clause(sent_C(cl(_,CN3,by(Cn3,V31,V32,V3,W3),_,_,_,_,_,_)),
true,Ref),
not(logically_erased(sent_C,Ref)),
!.
%%% Empty hyper-match.
proc_C(_,_,[],_,_,0,[],[],[],V3,[W3]) :- !.
%%% nucleus is not unit but hyper-match is ground.
proc_C(_,_,Cn2,V2,_,0,Cn2,[],[],V3,W3) :-
var(V2),
same_number_W1(Cn2,W3), !.
%%% Otherwise linearize the hyper-match.
%%% NOTE that we have already make the nucleus non-linearized by setting
%%% V11 = V12
%%% before.
proc_C(_,_,Cn2,V2,W2,CV3,Cn3,V31,V32,V2,W3) :-
linearize_term(Cn2,Cn3,V31,V32),
w1_w2(W2,W3),
compute_V_lits(W3,0,CV3).
%%% Take as many entries as Cn2 from W2.
same_number_W1([_|Cn2],[_|Ws3]) :-
same_number_W1(Cn2,Ws3).
same_number_W1([],[]).
%%% Calculate new W1 from old W1.
w1_w2([W2|Ws2],[W3|Ws3]) :-
vars_V1_V2(W2,W3), !,
w1_w2(Ws2,Ws3).
w1_w2([],[]).
%%% Calculate vars tail for hyper-matches.
%%% Unit hyper-match.
make_varstail(1,V1,[_],V1) :- !.
%%% empty hyper-match.
make_varstail(_,_,[],V1) :- !.
make_varstail(_,_,W1,V2) :-
vars_W1_V1(W1,V2), !.
%%% vars_V1_V2 calculates variable list V2 from a variable list V1.
%%% V1 is already a form with tail.
%%% V1 is for a hyper-match, it may not be a variable list due to the
%%% unification of nucleus to its mates.
%%% V2 keeps the tail of V1.
vars_V1_V2(V1,V1) :- var(V1), !.
vars_V1_V2(V1,V2) :-
vars_V1_V2(V1,[],_,V2,Hole), !.
vars_V1_V2(V,_,_,Hole,Hole) :- var(V), !.
vars_V1_V2([L1|Ls1],Sofar_in,Sofar_out,V2,Hole) :-
vars_V1_V2_elem(L1,Sofar_in,Sofar_mid,V2,Hole1),
!,
vars_V1_V2(Ls1,Sofar_mid,Sofar_out,Hole1,Hole).
vars_V1_V2_elem(Term, Sofar_in, Sofar_in,Hole,Hole) :-
atomic(Term), !.
vars_V1_V2_elem(Term, Sofar_in, Sofar_in,Hole,Hole) :-
var(Term),
identical_member(Term, Sofar_in), !.
vars_V1_V2_elem(Term, Sofar_in, [Term|Sofar_in],[Term|Hole],Hole) :-
var(Term), !.
vars_V1_V2_elem(Term, Sofar_in, Sofar_out,V2,Hole) :-
functor(Term, _, N),
vars_V1_V2_elem(0,N,Term,Sofar_in,Sofar_out,V2,Hole).
vars_V1_V2_elem(N,N,_,S,S,Hole,Hole) :- !.
vars_V1_V2_elem(N1,N2,Term,Sofar_in,Sofar_out,V2,Hole) :-
M is N1+1,
arg(M,Term,Arg),
vars_V1_V2_elem(Arg,Sofar_in,Sofar_mid,V2,Hole1),
!,
vars_V1_V2_elem(M,N2,Term,Sofar_mid,Sofar_out,Hole1,Hole).
%%% vars_W1_V1 calculates V1 from W1.
vars_W1_V1(W1,V1) :-
vars_W1_V1(W1,[],_,V1,Hole).
vars_W1_V1([W1|Ws1],Sofar_In,Sofar_Out,V1,Hole) :-
vars_W1_V1_2(W1,Sofar_In,Sofar_Mid,V1,Hole1), !,
vars_W1_V1(Ws1,Sofar_Mid,Sofar_Out,Hole1,Hole).
vars_W1_V1([],_,_,Hole,Hole).
vars_W1_V1_2(W1,Sofar_In,Sofar_In,Hole,Hole) :- var(W1), !.
vars_W1_V1_2([W1|Ws1],Sofar_In,Sofar_Out,V1,Hole) :-
vars_V1_V2_elem(W1,Sofar_In,Sofar_Mid,V1,Hole1),
!,
vars_W1_V1_2(Ws1,Sofar_Mid,Sofar_Out,Hole1,Hole).
%%% DUPLICATE CHECKING FOR HM
%%%
%%% If no dliding priority is specified, then we don't need to check the
%%% priorities, check the number of hyper-matches, and so forth.
noslide_update_HM(_,_,CSize2,CP2,F2,Cn2,V2,_,CS2,CR2) :-
update_HM(CSize2,CP2,F2,Cn2,V2,CS2,CR2), !.
noslide_update_HM(_,_,_,_,_,Cn2,_,_,_,_) :-
(check_unit_conflict_C(Cn2); check_unit_conflict_HM(Cn2)),
!,
assert_tryresult('unsatisfiable'),
assert_prooftype('UC').
noslide_update_HM(RefNucl,U,CSize2,CP2,F2,Cn2,V2,W1,CS2,CR2) :-
proc_C(U,RefNucl,Cn2,V2,W1,CN2,Cn3,V21,V22,V3,W2),
!, check_literalbound(hm,CN2,CS2),
print_HM(Cn2,V2,CS2,CR2,F2),
asserta(sent_HM(cl(CSize2,CN2,by(Cn3,V21,V22,V3,W2),
0,CS2,CR2,0,F2,CP2))), !.
%%% First check sent_HM, then sent_T, then sent_C.
%%% The order is important.
update_HM(CSize2,CP2,F2,Cn2,V2,CS2,CR2) :-
const_list(V2),
update_HM(CSize2,CP2,F2,Cn2,CS2,CR2).
update_HM(CSize2,CP2,F2,Cn2,CS2,CR2) :-
update_HM_1(CSize2,CP2,F2,Cn2,CS2,CR2).
update_HM(CSize2,CP2,F2,Cn2,CS2,CR2) :-
update_HM_2(CSize2,CP2,F2,Cn2,CS2,CR2).
update_HM(CSize2,CP2,F2,Cn2,CS2,CR2) :-
update_HM_3(CSize2,CP2,F2,Cn2,CS2,CR2).
%%% Duplicate check against sent_HM.
update_HM_1(CSize1,pr(_,_,PL1,_,PX1),F1,Cn1,CS1,CR1) :-
sent_HM(cl(CSize1,_,by(Cn1,V21,V21,V2,_),_,
CS2,CR2,_,F2,pr(_,_,PL2,_,PX2))),
const_list(V2),
min_ind(PL2,PL1,PL3,Up),
min_ind(PX2,PX1,PX3,Up),
min_Flags_ind(F2,F1,F3,Up),
max_CS_ind(CS2,CS1,CS3,Up),
min_CR_ind(CR2,CR1,CR3,Up),
update_HM_11(Up,Cn1,PL3,PX3,F3,CS3,CR3).
update_HM_11(n,_,_,_,_,_,_) :- !.
update_HM_11(_,Cn1,PL3,PX3,F3,CS3,CR3) :-
clause(sent_HM(cl(_,_,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,Ref2),
const_list(V2),
clause(sent_HM(cl(CSize2,CN2,BY_2,CI2,_,_,CT2,_,pr(PS2,PD2,_,_,_))),
true,Ref2),
erase(Ref2),
priority_NewPR(CR3,PR3),
asserta(sent_HM(cl(CSize2,CN2,BY_2,CI2,CS3,CR3,CT2,F3,
pr(PS2,PD2,PL3,PR3,PX3)))).
%%% Duplicate check against sent_T.
update_HM_2(CSize1,pr(_,_,PL1,_,PX1),F1,Cn1,CS1,CR1) :-
sent_T(cl(CSize1,_,by(Cn1,V21,V21,V2,_),_,
CS2,CR2,_,F2,pr(_,_,PL2,_,PX2))),
const_list(V2),
min_ind(PL2,PL1,PL3,Up),
min_ind(PX2,PX1,PX3,Up),
min_Flags_ind(F2,F1,F3,Up),
max_CS_ind(CS2,CS1,CS3,Up),
min_CR_ind(CR2,CR1,CR3,Up),
update_HM_21(Up,Cn1,PL3,PX3,F3,CS3,CR3).
update_HM_21(n,_,_,_,_,_,_) :- !.
update_HM_21(_,Cn1,PL3,PX3,F3,CS3,CR3) :-
clause(sent_T(cl(_,_,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,Ref2),
const_list(V2),
clause(sent_T(cl(CSize2,CN2,BY_2,_,_,CI2,CT2,_,pr(PS2,PD2,_,_,_))),
true,Ref2),
erase(Ref2),
priority_NewPR(CR3,PR3),
asserta(sent_T(cl(CSize2,CN2,BY_2,CI2,CS3,CR3,CT2,F3,
pr(PS2,PD2,PL3,PR3,PX3)))).
%%% Duplicate check against sent_C.
%%% If a duplicate found, store the hyper-match as sent_T.
update_HM_3(CSize1,CP1,F1,Cn1,CS1,CR1) :-
sent_C(cl(CSize1,_,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),
const_list(V2),
clause(sent_C(cl(_,_,by(Cn1,V31,V31,V3,_),_,_,_,_,_,_)),
true,Ref2),
const_list(V3),
not(logically_erased(sent_C,Ref2)),
clause(sent_C(cl(_,CN1,BY_2,_,_,_,_,_,_)),true,Ref2),
asserta(sent_T(cl(CSize1,CN1,BY_2,0,CS1,CR1,0,F1,CP1))).
%%% RELEVANCE TEST
%%%
%%% relevance test.
%%% Two stages:
%%% 1. Test user distance =< RelBound
%%% 2. Test CR2 >= CR1
%%%
check_rel_clause(Ds1,C,Ds2) :-
check_rel_clause1(Ds1,C,Ds2),
!.
check_rel_clause(_,_,_) :-
!, is_time_overflow.
check_rel_clause1(ds(R11,R12,R13),Cn2,ds(R21,R22,R23)) :-
relevance_bound(RelBound),
check_rel_u(R21,RelBound),
!,
distance_equalR(R11,R12,R13,Cn2,RelBound),
!,
distance_ge(R21,R22,R23,R11,R12,R13), !.
check_rel_u(R,RelBound) :-
R =< RelBound, !.
check_rel_u(_,_) :-
assert_once(over_relevance), !, fail.
%%% if max(B+F,U) = RelBound,
%%% then
%%% 1. if U = RelBound, it should be unit.
%%% 2. if B = RelBound, it should be all positive.
%%% 3. if F = RelBound, it should be all negative.
distance_equalR(RelBound,_,_,[_,_|_],RelBound) :- !, fail.
distance_equalR(_,RelBound,_,Cn2,RelBound) :- \+ posclause(Cn2), !, fail.
distance_equalR(_,_,RelBound,Cn2,RelBound) :- \+ negclause(Cn2), !, fail.
distance_equalR(_,_,_,_,_).
distance_ge(R21,R22,R23,R11,R12,R13) :-
R21 >= R11, !,
R22 >= R12, !,
R23 >= R13, !.
%%% check max(B+F,U) =< relevance after each literal match.
%%% B+F is monotonically increasing, so there is no problem for B+F.
%%% But U is monotonically decreasing. This cause problem.
%%% So if max(B+F,U) test fails after the current literal matching, it
%%% is not necessarily that
%%% max(B+F,U)
%%% test will fail at the end of hyper-matching of a nucleus.
%%%
%%% Therefore, the only thing that we can do for testing the relevance
%%% after each literal matching is checking B+F. This automatically
%%% consider the case that the nucleus is in support set.
check_rel_bf(ds(_,R12,R13)) :-
relevance_bound(RelBound),
YY is R12 + R13, !,
check_rel_bf_2(YY,RelBound), !.
check_rel_bf_2(YY,RelBound) :-
YY =< RelBound, !.
check_rel_bf_2(_,_) :-
assert_once(over_relevance), !, fail.
%%% UPDATE CS AND CR
%%%
%%% onematch_SR updates the values of CS and CR.
%%% onematch_S updates the values of CS.
%%% For F, B, and UR:
%%% if CS1 has 1, then CS2 has the same as CSM.
%%% if CS1 has 0, then CS2 has 0.
%%% For U:
%%% if CS1 has 1, then CS2 has 1.
%%% if CS1 has 0, then CS2 has the same as CSM.
%%% onematch_R updates the values of CR.
%%% if CR1 has 0, then CR2 has 0.
%%% if CR1 has nonzero, then CR2 is CRM + 1.
onematch_SR(Ln1,CS1,CR1,CSM,CRM,CS2,CR2) :-
onematch_S(Ln1,CS1,CSM,CS2),
onematch_R(CSM,Ln1,CR1,CRM,CR2), !.
onematch_S(Ln1,sp(S11,S12,S13),sp(S21,S22,S23),sp(S31,S32,S33)) :-
one_dominate(S11,S21,S31),
zero_dominate_bf(Ln1,S12,S22,S32,S13,S23,S33).
%%% If one of inputs is 1, then the output is 1.
one_dominate(1,_,1) :- !.
one_dominate(_,S,S).
%%% If one of inputs is 0, then the output is 0.
zero_dominate_bf(Ln1,S12,S22,S32,S13,_,S13) :-
negative_lit(Ln1),
zero_dominate(S12,S22,S32).
zero_dominate_bf(Ln1,S12,_,S12,S13,S23,S33) :-
zero_dominate(S13,S23,S33).
zero_dominate(0,_,0) :- !.
zero_dominate(_,S1,S1).
onematch_R(sp(S21,_,_),Ln1,ds(R11,R12,R13),
ds(R21,R22,R23),ds(R31,R32,R33)) :-
cal_ud(S21,R11,R21,R31),
cal_bfd(Ln1,R12,R22,R32,R13,R23,R33), !.
cal_ud(_,0,_,0) :- !.
%%% If the mate is user supported,
cal_ud(1,R11,R21,R31) :-
RR is R21 + 1,
minimum(R11,RR,R31).
%%% If the mate is not user supported,
%%% user distance = current user distance
cal_ud(0,R11,_,R11).
cal_bfd(Ln1,R12,R22,R32,R13,_,R13) :-
negative_lit(Ln1),
cal_bf(R12,R22,R32), !.
cal_bfd(_,R12,_,R12,R13,R23,R33) :-
cal_bf(R13,R23,R33).
cal_bf(0,_,0) :- !.
cal_bf(R1,R2,R3) :-
RR is R2 + 1,
maximum(R1,RR,R3).
%%% Make adustments of the user distance.
adjust_userdist(ds(X,R12,R13),ds(R11,_,_),ds(R11,R12,R13)) :-
infinity(X), !.
adjust_userdist(CRM,_,CRM) :- !.
%%% GENERAL MATCHING
%%%
%%% Find one mate at a time.
%%%
%%% No reference as input, prolog does this very fast.
unify_mate_occurscheck(0,NLn1,T,CS2,CR2) :-
lit_S(T,lby(NLn1,V21,V22,_),CS2,CR2),
unify_lists(V21,V22).
unify_mate_occurscheck(1,NLn1,T,CS2,CR2) :-
lit_G(T,lby(NLn1,V21,V22,_),CS2,CR2),
unify_lists(V21,V22).
%%% With reference as input, so unify one at a time.
unify_mate_occurscheck(0,NLn1,T,CS2,CR2,Ref2) :-
clause(lit_S(T,lby(NLn1,V21,V22,_),CS2,CR2),true,Ref2),
unify_lists(V21,V22).
unify_mate_occurscheck(1,NLn1,T,CS2,CR2,Ref2) :-
clause(lit_G(T,lby(NLn1,V21,V22,_),CS2,CR2),true,Ref2),
unify_lists(V21,V22).
%%% HYPER-MATCHING LITERALS
%%%
%%% Matching one literal at a time.
%%%
hm_literals([Ln1|Lns1],WO1,U,RefNucl,CS1,CR1,Mtype,
RLists,Ts,CS2,CR2,Cn1,LnkLits) :-
hm_lit_reorder_3(WO1,[Ln1|Lns1],Ts,W1,Ws1,L1,Ls1,T1,Ts1),
!,
hm_literal(U,RefNucl,L1,CS1,CR1,Mtype,RLists,T1,CSM,CRM,Cn1,LnkLits),
!, hm_literals(Ls1,Ws1,U,RefNucl,CSM,CRM,Mtype,RLists,Ts1,CS2,CR2,Cn1,
LnkLits).
hm_literals([L1|Ls1],[W1|Ws1],U,RefNucl,CS1,CR1,Mtype,
RLists,[T1|Ts1],CS2,CR2,Cn1,LnkLits) :-
hm_literal(U,RefNucl,L1,CS1,CR1,Mtype,RLists,T1,CSM,CRM,Cn1,LnkLits),
w1_w2(Ws1,Ws2),
hm_literals(Ls1,Ws2,U,RefNucl,CSM,CRM,Mtype,RLists,Ts1,CS2,CR2,Cn1,
LnkLits).
hm_literals([],_,_,_,CS2,CR2,_,_,_,CS2,CR2,_,_).
%%% Matching one literal.
%%% hm_literal hyper-match a literal.
%%% Inputs:
%%% U: 1 if the nucleus is unit clause. We don't instantiate
%%% the nucleus, but have to find maximum B and F, minimum
%%% U.
%%% 0 if the nucleus is not unit clause.
%%% RefNucl: The reference for the nucleus. It is used for finding
%%% maximum B and F, minimum U for a unit nucleus such that
%%% we don't need to make copies for the unit nucleus.
%%% Ln1: A literal of the nucleus to be matched.
%%% CS1: Supported status.
%%% CR1: Distance.
%%% Mtype: 0 for Lit_S.
%%% 1 for Lit_G.
%%% RLists: The literal list for unit nucleus.
%%% Outputs:
%%% T: 1 if the mate is unit clause.
%%% 0 if the mate is not unit clause.
%%% CS2: Supported status.
%%% CR2: Distance.
%%% Check if relevance overflowed.
%%% Check if backward or forward supported if it is required so.
hm_literal(U,RefNucl,Ln1,CS1,CR1,Mtype,RLists,T,CS2,CR2,Cn1,LnkLits) :-
negate(Ln1,L1),
rewrite_lit(L1,Sp,Ds,1,L2,_),
negate(L2,Ln2),
hm_literal_1(U,RefNucl,Ln2,CS1,CR1,Mtype,RLists,T,CS2,CR2),
update_LnkLits(Cn1,Ln1,LnkLits,T),
check_rel_bf(CR2),
check_supp_bf(CS2),
hm_literal_2(Cn1,CS2,CR2,LnkLits).
hm_literal_2(_,_,_,LnkLits) :-
all_literals_linked(LnkLits),
!.
hm_literal_2(Cn1,Sp,Ds,LnkLits) :-
rewrite_clause_np(Cn1,Sp,Ds,1,Cn2,_),
hm_literal_4(Cn2,Sp,Ds,LnkLits),
hm_literal_12(Cn2),
hm_literal_14(Cn2,LnkLits),
hm_literal_3(Cn2,Sp,Ds,LnkLits),
!.
hm_literal_3(Cn1,Sp,Ds,LnkLits) :-
early_unit_subsumpt(Cn1,Sp,Ds,LnkLits),
!,
is_time_overflow.
hm_literal_3(_,_,_,_).
hm_literal_4(_,_,_,_) :-
not(fixed_priority),
not(slidepriority),
!.
hm_literal_4(Cn1,Sp,Ds,LnkLits) :-
hm_literal_5(Cn1,Sp,Ds,LnkLits),
!.
hm_literal_5(Cn1,Sp,Ds,LnkLits) :-
hm_literal_6(Cn1,Cn2,LnkLits),
hm_literal_8(Cn2,Cn3),
calculate_priority_clause(Cn3,Sp,Ds,Pr),
priority_bound(PrioBound),
check_prioritybound(Pr,PrioBound),
(fast_priority_update -> (
update_priority_structure(Pr)
); true),
!.
hm_literal_5(_,_,_,_) :-
!,
is_time_overflow.
hm_literal_6(C1,C2,LnkLits) :-
safe_early_priority_test,
!,
hm_literal_7(C1,C2,LnkLits),
!.
hm_literal_6(C,C,_).
hm_literal_7([],[],[]).
hm_literal_7([L|Ls1],Ls2,[F|LnkLits]) :-
var(F),
negate(L,NL),
not(not(unify_mate_occurscheck(_,NL,1,_,_))),
!,
hm_literal_7(Ls1,Ls2,LnkLits).
hm_literal_7([L|Ls1],Ls2,[F|LnkLits]) :-
F==u,
!,
hm_literal_7(Ls1,Ls2,LnkLits).
hm_literal_7([L|Ls1],[L|Ls2],[_|LnkLits]) :-
!,
hm_literal_7(Ls1,Ls2,LnkLits).
hm_literal_8(C1,C2) :-
safe_early_priority_test,
size_by_clause,
not(size_coef(0)),
!,
hm_literal_9(C1,C2),
!.
hm_literal_8(C1,C2) :-
safe_early_priority_test,
not(literal_coef(0)),
!,
hm_literal_9(C1,C2),
!.
hm_literal_8(C,C).
hm_literal_9([],[]).
hm_literal_9([L|Ls1],[L|Ls2]) :-
hm_literal_10(L,Ls1,Ls3),
!,
hm_literal_9(Ls3,Ls2).
hm_literal_10(_,[],[]).
hm_literal_10(L,[L1|Ls1],Ls2) :-
not(not(unify(L,L1))),
!,
hm_literal_11(L,L1,L2),
hm_literal_10(L2,Ls1,Ls2).
hm_literal_10(L,[L1|Ls1],[L1|Ls2]) :-
hm_literal_10(L,Ls1,Ls2).
hm_literal_11(L1,L2,L1) :-
calculate_priority_clause([L1],sp(1,1,1),ds(0,0,0),N1),
calculate_priority_clause([L2],sp(1,1,1),ds(0,0,0),N2),
N1<N2,
!.
hm_literal_11(L1,L2,L2).
hm_literal_12(C) :-
early_tautology_test,
!,
hm_literal_13(C),
!.
hm_literal_12(_).
hm_literal_13(C) :-
fol_tautology_clause(C),
!,
increment_counter(counter1,1),
is_time_overflow.
hm_literal_13(_).
hm_literal_14(_,_) :-
not(duplicate_partial_instance_test),
!.
hm_literal_14(C,LnkLits) :-
hm_literal_15(C,LnkLits,C1,LnkLits1),
vars_tail(C1,V),
not(not(hm_literal_16(C1,V,LnkLits1))),
hm_literal_17(C1,P),
assert(part_inst(C1,V,LnkLits1,P)),
!.
hm_literal_14(_,_) :-
increment_counter(counter2,1),
is_time_overflow.
hm_literal_15([],[],[],[]).
hm_literal_15([L|Ls],[F|LnkLits],[L|Ls1],[0|LnkLits1]) :-
var(F),
!,
hm_literal_15(Ls,LnkLits,Ls1,LnkLits1).
hm_literal_15([_|Ls],[u|LnkLits],Ls1,LnkLits1) :-
!,
hm_literal_15(Ls,LnkLits,Ls1,LnkLits1).
hm_literal_15([L|Ls],[n|LnkLits],[L|Ls1],[1|LnkLits1]) :-
!,
hm_literal_15(Ls,LnkLits,Ls1,LnkLits1).
hm_literal_16(C,V,LnkLits) :-
delete_all_instances,
!,
const_list(V),
not(part_inst(C,_,LnkLits,_)),
!.
hm_literal_16(C,V,LnkLits) :-
const_list(V),
not(part_inst(C,V,LnkLits,_)).
hm_literal_17(C,P) :-
slidepriority,
!,
calculate_priority_clause(C,sp(0,0,0),ds(0,0,0),pr(_,_,_,_,P)).
hm_literal_17(_,0).
%%% Match the specified literal.
%%% If the literal is unit clause, calculate the minimum or maximum for
%%% the informations. No backtracking for more hyper-matches.
hm_literal_1(1,RefNucl,Ln1,CS1,CR1,Mtype,RLists,T,CS2,CR2) :-
unit_mate(RefNucl,Mtype,RLists,T,CSM,CRM),
onematch_SR(Ln1,CS1,CR1,CSM,CRM,CS2,CR2), !.
%%% If the literal is ground, calculate the minimum or maximum for
%%% the informations. No backtracking for more hyper-matches.
hm_literal_1(0,_,Ln1,CS1,CR1,Mtype,RLists,T,CS2,CR2) :-
numbervars(Ln1,0,0),
!,
ground_mate(Mtype,Ln1,RLists,T,CSM,CRM),
onematch_SR(Ln1,CS1,CR1,CSM,CRM,CS2,CR2), !.
%%% Otherwise, with backtracking for more hyper-matches.
hm_literal_1(0,_,Ln1,CS1,CR1,Mtype,_,T,CS2,CR2) :-
unify_mate_occurscheck(Mtype,Ln1,T,CSM,CRM),
onematch_SR(Ln1,CS1,CR1,CSM,CRM,CS2,CR2).
%%% Find the informations for unit clause.
unit_mate(RefNucl,Mtype,RLists,T,CS2,CR2) :-
unit_mate_first(Mtype,RefNucl,RLists,TF,CSF,CRF,RListsR),
unit_mate_min(Mtype,RefNucl,TF,CSF,CRF,RListsR,T,CS2,CR2).
unit_mate_first(Mtype,RefNucl,RLists,TF,CSF,CRF,RListsR) :-
find_unitclause(RefNucl,NLn1),
mate_first(Mtype,NLn1,RLists,TF,CSF,CRF,RListsR).
unit_mate_min(Mtype,RefNucl,TF,CSF,CRF,RLists,T,CS2,CR2) :-
unit_mate_first(Mtype,RefNucl,RLists,T1,CS1,CR1,RListsR),
mate_min_1(TF,CSF,CRF,T1,CS1,CR1,TM,CSM,CRM),
!,
unit_mate_min(Mtype,RefNucl,TM,CSM,CRM,RListsR,T,CS2,CR2).
unit_mate_min(_,_,T,CS2,CR2,_,T,CS2,CR2).
%%% Find another copy of unit clause, so that the next matching can be
%%% done without being affected by the previous matching.
%%% Note that the unit clause is found even if has been logically erased.
find_unitclause(RefNucl,NLn) :-
clause(sent_C(cl(_,_,by([ULn],V11,V11,_,_),_,_,_,_,_,_)),
true,RefNucl),
negate(ULn,NLn), !.
%%% Find informations for a ground literal.
ground_mate(Mtype,Ln1,RLists,T,CS2,CR2) :-
mate_first(Mtype,Ln1,RLists,TF,CSF,CRF,RListsR),
mate_min(Mtype,Ln1,TF,CSF,CRF,RListsR,T,CS2,CR2).
%%% Find the first match.
mate_first(Mtype,Ln1,[RList|RLists],TF,CSF,CRF,RLists) :-
unify_mate_occurscheck(Mtype,Ln1,TF,CSF,CRF,RList).
mate_first(Mtype,Ln1,[RList|RLists],TF,CSF,CRF,RestLists) :-
mate_first(Mtype,Ln1,RLists,TF,CSF,CRF,RestLists).
%%% Find the other matches for calculating minimum or maximum informations.
mate_min(Mtype,Ln1,TF,CSF,CRF,RLists,T,CS2,CR2) :-
mate_first(Mtype,Ln1,RLists,T1,CS1,CR1,RListsR),
mate_min_1(TF,CSF,CRF,T1,CS1,CR1,TM,CSM,CRM),
!,
mate_min(Mtype,Ln1,TM,CSM,CRM,RListsR,T,CS2,CR2).
mate_min(_,_,T,CS2,CR2,_,T,CS2,CR2).
mate_min_1(TF,CSF,CRF,T1,CS1,CR1,TM,CSM,CRM) :-
binary_max(TF,T1,TM),
max_CS(CSF,CS1,CSM),
min_CR(CRF,CR1,CRM).
%%% check literal bound.
check_literalbound(hm,CV2,CS2) :-
check_all_literalbound(CV2), !,
check_user_literalbound(CV2,CS2), !,
check_back_literalbound(CV2,CS2), !,
check_for_literalbound(CV2,CS2), !.
check_literalbound(_,_,_).
%%% Check general literal bound.
check_all_literalbound(CV2) :-
literal_bound(LitBdV),
!, check_clause_literalbound(CV2,LitBdV).
check_all_literalbound(_).
%%% Check literal bound for user supported hyper-matches.
check_user_literalbound(CV2,sp(1,_,_)) :-
user_literalbound(ULitBdV),
!, check_clause_literalbound(CV2,ULitBdV).
check_user_literalbound(_,_).
%%% Check literal bound for backward supported hyper-matches.
check_back_literalbound(CV2,sp(_,1,_)) :-
back_literalbound(BLitBdV),
!, check_clause_literalbound(CV2,BLitBdV).
check_back_literalbound(_,_).
%%% Check literal bound for forward supported hyper-matches.
check_for_literalbound(CV2,sp(_,_,1)) :-
for_literalbound(FLitBdV),
!, check_clause_literalbound(CV2,FLitBdV).
check_for_literalbound(_,_).
%%% If the bound is 0, that means no literal bound is enforced.
check_clause_literalbound(_,-1).
check_clause_literalbound(Ln,LitBdV) :-
Ln =< LitBdV, !.
check_clause_literalbound(_,_) :-
assert_once(over_litbound), !, fail.
%%% check if it is desiredly supported for B and F.
check_supp_bf(sp(_,0,_)) :-
current_support(sup(_,1,_,_)), !, fail.
check_supp_bf(sp(_,_,0)) :-
current_support(sup(_,_,1,_)), !, fail.
check_supp_bf(_) :- !.
%%% check if it is desiredly supported for U.
check_supp_u(sp(0,_,_)) :-
current_support(sup(1,_,_,_)), !, fail.
check_supp_u(_) :- !.
%%% Determine the initial information fields for hyper-matches.
clause_part2(sp(S11,_,_),ds(0,R12,R13),sp(S11,1,1),ds(0,R12,R13)) :- !.
clause_part2(sp(S11,_,_),ds(_,R12,R13),sp(S11,1,1),ds(X,R12,R13)) :-
infinity(X), !.
%%% Separate the literals of the nucleus into two groups. One group should be
%%% matched by supported mates.
%%% Note that Cn1 is already negated.
matord(Cn1,Ord1,Ord2,W1,WO1,WO2,T1,TOrd1,TOrd2) :-
current_support(Sup),
matord(Sup,Cn1,Ord1,Ord2,W1,WO1,WO2,T1,TOrd1,TOrd2).
matord(Sup,[G|Gs],L1,L2,[W1|Ws1],WO1,WO2,[X|Xs],Y1,Y2) :-
matord_1(Sup,G,L1,L2,Ls1,Ls2,W1,WO1,WO2,WOs1,WOs2,X,Y1,Y2,Ys1,Ys2),
!,
matord(Sup,Gs,Ls1,Ls2,Ws1,WOs1,WOs2,Xs,Ys1,Ys2).
matord(_,[],[],[],[],[],[],[],[],[]).
matord_1(sup(1,0,0,0),G,[G|Ls1],Ls2,Ls1,Ls2,W,[W|Ws1],Ws2,
Ws1,Ws2,X,[X|Ys1],Ys2,Ys1,Ys2).
matord_1(sup(_,_,_,1),G,[G|Ls1],Ls2,Ls1,Ls2,W,[W|Ws1],Ws2,
Ws1,Ws2,X,[X|Ys1],Ys2,Ys1,Ys2).
matord_1(sup(_,1,_,_),G,[G|Ls1],Ls2,Ls1,Ls2,W,[W|Ws1],Ws2,
Ws1,Ws2,X,[X|Ys1],Ys2,Ys1,Ys2) :-
negative_lit(G).
matord_1(sup(_,1,_,_),G,Ls1,[G|Ls2],Ls1,Ls2,W,Ws1,[W|Ws2],
Ws1,Ws2,X,Ys1,[X|Ys2],Ys1,Ys2).
matord_1(_,G,[G|Ls1],Ls2,Ls1,Ls2,W,[W|Ws1],Ws2,
Ws1,Ws2,X,[X|Ys1],Ys2,Ys1,Ys2) :-
\+ negative_lit(G).
matord_1(_,G,Ls1,[G|Ls2],Ls1,Ls2,W,Ws1,[W|Ws2],
Ws1,Ws2,X,Ys1,[X|Ys2],Ys1,Ys2).
%%% Throw away nucleus.
%%% If the nucleus was generated from replace rules, don't throw away.
%%% If a nucleus is supported by the current strategies, then it can be
%%% thrown away.
check_throw_nucleus(1,_,_,_,_) :- !.
check_throw_nucleus(0,1,_,_,_) :- !.
check_throw_nucleus(0,_,Cn1,CS1,RefNucl) :-
check_throw_nucleus(Cn1,CS1),
logically_erase(sent_C,RefNucl), !.
check_throw_nucleus(_,_,_,_,_).
check_throw_nucleus(Cn1,sp(S11,S12,S13)) :-
current_support(sup(S21,S22,S23,S24)), !,
one_dominate(S11,S21,S11), !,
one_dominate(S12,S22,S12), !,
one_dominate(S13,S23,S13), !,
check_throw_nucleus_r(Cn1,S24).
check_throw_nucleus_r([_,_|_],1) :- !, fail.
check_throw_nucleus_r(_,_).
hm_lit_reorder_3(Ws,Ls,Ts,W1,Ws1,L1,Ls1,T1,Ts1) :-
hl_literal_reordering,
!, sep_gr_lit_3(Ws,Ls,Ts,W1,Ws1,L1,Ls1,T1,Ts1).
%%% Delete non-user rewrite rules whose lhs or rhs priority is too large.
rmrwr_prio(P) :-
rwr((S->T),V,F,0),
rmrwr_prio_1(S,T,P),
erase_rewrite_rule(rwr((S->T),V,F,0)),
assert_once(over_priohm),
fail.
rmrwr_prio(P) :-
rwr(S=T,V,F,0),
rmrwr_prio_1(S,T,P),
erase_rewrite_rule(rwr(S=T,V,F,0)),
assert_once(over_priohm),
fail.
rmrwr_prio(_).
rmrwr_prio_1(S,_,P) :-
calculate_priority_clause([S],sp(0,0,0),ds(0,0,0),pr(_,_,_,_,P1)),
P1 > P,
!.
rmrwr_prio_1(_,T,P) :-
calculate_priority_clause([T],sp(0,0,0),ds(0,0,0),pr(_,_,_,_,P1)),
P1 > P,
!.
%%% Delete partial instances whose priority are too large.
rmpartinst_prio(P) :-
clause(part_inst(C,V,LnkLits,P1),true,Ref),
P1 > P,
erase(Ref),
fail.
rmpartinst_prio(_).
%%% Determine if a partial instance can be rejected by equality early unit
%%% subsumption. We first try early unit subsumption and then equality
%%% early unit subsumption. Early_unit_subsumpt suceeds if the partial
%%% instance can be rejected.
early_unit_subsumpt(C,_,_,_) :-
early_unit_subsumption,
not(not(early_unit_subsumpt_4(C))),
increment_counter(counter3,1),
!.
early_unit_subsumpt(C,Sp,Ds,LnkLits) :-
equality_early_unit_subsumption,
not(not(early_unit_subsumpt_1(C,Sp,Ds,LnkLits))),
increment_counter(counter4,1),
!.
early_unit_subsumpt_1(C,Sp,Ds,LnkLits) :-
early_unit_subsumpt_2(C,LnkLits),
early_unit_subsumpt_3(C,LnkLits,_),
rewrite_clause_np(C,Sp,Ds,1,C1,_),
early_unit_subsumpt_4(C1),
!.
early_unit_subsumpt_2([L|Ls],[F|LnkLits]) :-
var(F),
!,
early_unit_subsumpt_2(Ls,LnkLits).
early_unit_subsumpt_2([not S=T|Ls],[F|LnkLits]) :-
S==T,
!,
early_unit_subsumpt_2(Ls,LnkLits).
early_unit_subsumpt_2(_,_).
early_unit_subsumpt_3([],[],F) :-
nonvar(F).
early_unit_subsumpt_3([L|Ls],[F|LnkLits],_) :-
var(F),
negate(L,NL),
unify(NL,X=X),
!,
early_unit_subsumpt_3(Ls,LnkLits,c).
early_unit_subsumpt_3([_|Ls],[_|LnkLits],F) :-
!,
early_unit_subsumpt_3(Ls,LnkLits,F).
early_unit_subsumpt_4(C) :-
vars_tail(C,V),
const_list(V),
early_unit_subsumpt_5(C),
!.
early_unit_subsumpt_5([L|_]) :-
sent_C(cl(_,_,by([L],V,V,_,_),_,_,_,_,_,_)),
!.
early_unit_subsumpt_5([L|_]) :-
sent_HM(cl(_,_,by([L],V,V,_,_),_,_,_,_,_,_)),
!.
early_unit_subsumpt_5([_|Ls]) :-
!,
early_unit_subsumpt_5(Ls).
%%% Create a linked literals list.
create_LnkLits([],[]).
create_LnkLits([_|Ls],[_|LnkLits]) :-
!,
create_LnkLits(Ls,LnkLits).
%%% Update a linked literals list. Note that NL is the negation of the literal
%%% being linked.
update_LnkLits(C,NL,LnkLits,T) :-
negate(NL,L),
update_LnkLits_1(C,L,LnkLits,T),
!.
update_LnkLits_1([L1|_],L2,[F|_],0) :-
var(F),
L1==L2,
!,
F=n.
update_LnkLits_1([L1|_],L2,[F|_],1) :-
var(F),
L1==L2,
!,
F=u.
update_LnkLits_1([_|Ls],L,[_|LnkLits],T) :-
!,
update_LnkLits_1(Ls,L,LnkLits,T).
%%% Determine if all literals have been linked.
all_literals_linked([]).
all_literals_linked([F|LnkLits]) :-
nonvar(F),
!,
all_literals_linked(LnkLits).
%%% Update priority stucture.
update_priority_structure(Pr) :-
slidepriority,
!,
total_numhm(TotalHM),
wu_bound(ExpectWU),
total_wu(TotalWU),
update_priority_structure_1(Pr,TotalHM,ExpectWU,TotalWU),
!.
update_priority_structure(_).
update_priority_structure_1(Pr,TotalHM,ExpectWU,TotalWU) :-
add_PT2(Pr,TotalWU,TotalWU1),
TotalWU1 =< ExpectWU,
update_numhm_wu(TotalHM,TotalWU1),
update_priowu(Pr),
!.
update_priority_structure_1(Pr,TotalHM,ExpectWU,TotalWU) :-
max_priority(MaxPrio),
retract_priowu(pr(_,_,_,_,MaxPrio),MaxNum,WUMaxPrio),
MaxPrio1 is MaxPrio - 1,
update_priority_bound(MaxPrio1),
rmhm_prio(MaxPrio),
rmrwr_prio(MaxPrio),
rmpartinst_prio(MaxPrio),
update_priority_structure_2(Pr,TotalHM,TotalWU,MaxPrio,MaxNum,
WUMaxPrio),
!.
update_priority_structure_2(pr(_,_,_,_,MaxPrio),TotalHM,TotalWU,MaxPrio,
MaxNum,WUMaxPrio) :-
TotalHM1 is TotalHM - MaxNum,
TotalWU1 is TotalWU - WUMaxPrio,
update_numhm_wu(TotalHM1,TotalWU1),
!.
update_priority_structure_2(Pr,TotalHM,TotalWU,MaxPrio,MaxNum,
WUMaxPrio) :-
TotalHM1 is TotalHM - MaxNum,
TotalWU1 is TotalWU - WUMaxPrio,
add_PT2(Pr,TotalWU1,TotalWU2),
update_numhm_wu(TotalHM1,TotalWU2),
update_priowu(Pr),
!.
